%!TEX root = ../rapport.tex

\chapter{Introduction}

In this work we develop an automatic method for visualization of
$\beta$-reduction graphs of lambda terms. The method has been implemented in
the programming language Python.

Until now, no software for reduction graph visualization existed. Researchers
wanting to visualize reduction graphs have therefore been limited to either
their own drawings or to what they can imagine. Since reduction graphs can be
very large, this posed a very tight constraint on what could be visually
presented.

In our opinion, software for this visualization task presents two primary
challenges: The drawn graphs must be \emph{informative} and
\emph{good-looking}. These two matters are not entirely independent of each
other; very often the particular layout of a graph's two-dimensional embedding
greatly reduces clutter and ``noise'', thus adding information. The opposite
can of course also be the case, which is why the two problems are
interchanged.

The intended user of the software is a theoretical computer scientist that
does research in the field of lambda calculus. Our hope is that researchers
can use this tool to gain new insight into the lambda calculus, and that it
will serve as a source of inspiration for new research because it offers a new
look at a well-known concept.

\section{A Brief History of the Lambda Calculus}

The lambda calculus was developed in the 1930s by Alonzo Church
\cite{Church1932}, contributing to the mathematical search for a foundation
for all mathematics. The attempt was unsuccesful, however, as it was possible
to derive meaningless equations by the Kleene-Rosser paradox
\cite{KleeneRosser1935}. After this setback, Church published a subset of the
theory, known as the \emph{untyped lambda calculus} \cite{Church1936}. This
part of the theory deals only with the concepts relevant for computation, and
does as such not try to lay out a general foundation for all mathematics.
Later on, Church also published a simple, typed version of his theory, known
as the \emph{simply typed lambda calculus} \cite{Church1940} in order to fix
some of the shortcomings of the original calculus. In the present work we deal
with the untyped version, whence the names ``lambda calculus'' and ``untyped
lambda calculus'' will be used as synonyms.

The untyped lambda calculus proved quite useful for computability theory.
Church proposed a definition of the notion ``effectively computable'' using
it, and Turing showed that his ``mechanical'' approach to computability in the
Turing machine is equivalent to Church's approach
\cite{Turing1936,Turing1937}. In the field of programming languages it was
also put to use, as it can be viewed as a Turing-complete programming
language, albeit very cumbersome to use. It is of course not intended to be
used as a ``regular'' programming language, rather, it provides a clean
mathematical framework and notation for language designers to reason about
programming language semantics. For instance, a formal semantics for Algol was
developed by translating the language into lambda calculus and then defining a
semantics for that \cite{Landin1965}.

\section{Expectations of the Reader}

The reader is expected to have a basic knowledge of graphs similar to
``Introduction to Graph Theory'' \cite{Trudeau1994}, along with basic
familiarity with Python similar to ``Python Programming: An Introduction to
Computer Science'' \cite{Zelle2004}. Knowledge of the lambda calculus from e.g.
\cite{Barendregt} Chapter 1, 2 and 3 is an advantage but not a requirement,
since the basic concepts relevant for this work are introduced in a later
chapter.
